Issue4768.agda:8,6-13
Not a finite domain: IsOne i
when checking that the pattern (i0 = i1) has type IsOne i
